$\forall$$T$:Type, ${\it as}$:($T$ List). ($\uparrow$null(${\it as}$)) $\Leftarrow\!\Rightarrow$ (${\it as}$ = [])